The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

natsFrom(N) → cons(N, n__natsFrom(n__s(N)))
fst(pair(XS, YS)) → XS
snd(pair(XS, YS)) → YS
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → u(splitAt(N, activate(XS)), N, X, activate(XS))
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS)
head(cons(N, XS)) → N
tail(cons(N, XS)) → activate(XS)
sel(N, XS) → head(afterNth(N, XS))
take(N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → snd(splitAt(N, XS))
natsFrom(X) → n__natsFrom(X)
s(X) → n__s(X)
activate(n__natsFrom(X)) → natsFrom(activate(X))
activate(n__s(X)) → s(activate(X))
activate(X) → X

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The following defined symbols can occur below the 0th argument of natsFrom: s, activate, natsFrom
The following defined symbols can occur below the 0th argument of head: splitAt, snd, afterNth
The following defined symbols can occur below the 0th argument of snd: splitAt
The following defined symbols can occur below the 0th argument of fst: splitAt
The following defined symbols can occur below the 0th argument of s: s, activate, natsFrom

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
splitAt(s(N), cons(X, XS)) → u(splitAt(N, activate(XS)), N, X, activate(XS))

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

natsFrom(N) → cons(N, n__natsFrom(n__s(N)))
splitAt(0, XS) → pair(nil, XS)
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS)
head(cons(N, XS)) → N
activate(X) → X
snd(pair(XS, YS)) → YS
take(N, XS) → fst(splitAt(N, XS))
activate(n__s(X)) → s(activate(X))
afterNth(N, XS) → snd(splitAt(N, XS))
activate(n__natsFrom(X)) → natsFrom(activate(X))
s(X) → n__s(X)
fst(pair(XS, YS)) → XS
tail(cons(N, XS)) → activate(XS)
natsFrom(X) → n__natsFrom(X)
sel(N, XS) → head(afterNth(N, XS))

Rewrite Strategy: INNERMOST

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

natsFrom(N) → cons(N, n__natsFrom(n__s(N))) [1]
splitAt(0, XS) → pair(nil, XS) [1]
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS) [1]
head(cons(N, XS)) → N [1]
activate(X) → X [1]
snd(pair(XS, YS)) → YS [1]
take(N, XS) → fst(splitAt(N, XS)) [1]
activate(n__s(X)) → s(activate(X)) [1]
afterNth(N, XS) → snd(splitAt(N, XS)) [1]
activate(n__natsFrom(X)) → natsFrom(activate(X)) [1]
s(X) → n__s(X) [1]
fst(pair(XS, YS)) → XS [1]
tail(cons(N, XS)) → activate(XS) [1]
natsFrom(X) → n__natsFrom(X) [1]
sel(N, XS) → head(afterNth(N, XS)) [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

natsFrom(N) → cons(N, n__natsFrom(n__s(N))) [1]
splitAt(0, XS) → pair(nil, XS) [1]
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS) [1]
head(cons(N, XS)) → N [1]
activate(X) → X [1]
snd(pair(XS, YS)) → YS [1]
take(N, XS) → fst(splitAt(N, XS)) [1]
activate(n__s(X)) → s(activate(X)) [1]
afterNth(N, XS) → snd(splitAt(N, XS)) [1]
activate(n__natsFrom(X)) → natsFrom(activate(X)) [1]
s(X) → n__s(X) [1]
fst(pair(XS, YS)) → XS [1]
tail(cons(N, XS)) → activate(XS) [1]
natsFrom(X) → n__natsFrom(X) [1]
sel(N, XS) → head(afterNth(N, XS)) [1]

The TRS has the following type information:

natsFrom :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil cons :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil n__natsFrom :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil n__s :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil splitAt :: 0 → n__s:n__natsFrom:cons:nil → pair 0 :: 0 pair :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil → pair nil :: n__s:n__natsFrom:cons:nil u :: pair → a → n__s:n__natsFrom:cons:nil → b → pair activate :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil head :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil snd :: pair → n__s:n__natsFrom:cons:nil take :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil fst :: pair → n__s:n__natsFrom:cons:nil s :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil afterNth :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil tail :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil sel :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

u
head
take
fst
tail
sel

(c) The following functions are completely defined:

splitAt
activate
afterNth
s
snd
natsFrom

Due to the following rules being added:

snd(v0) → nil [0]

And the following fresh constants:

const, const1, const2

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: natsFrom(N) → cons(N, n__natsFrom(n__s(N))) [1] splitAt(0, XS) → pair(nil, XS) [1] u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS) [1] head(cons(N, XS)) → N [1] activate(X) → X [1] snd(pair(XS, YS)) → YS [1] take(N, XS) → fst(splitAt(N, XS)) [1] activate(n__s(X)) → s(activate(X)) [1] afterNth(N, XS) → snd(splitAt(N, XS)) [1] activate(n__natsFrom(X)) → natsFrom(activate(X)) [1] s(X) → n__s(X) [1] fst(pair(XS, YS)) → XS [1] tail(cons(N, XS)) → activate(XS) [1] natsFrom(X) → n__natsFrom(X) [1] sel(N, XS) → head(afterNth(N, XS)) [1] snd(v0) → nil [0] The TRS has the following type information: natsFrom :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil cons :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil n__natsFrom :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil n__s :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil splitAt :: 0 → n__s:n__natsFrom:cons:nil → pair 0 :: 0 pair :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil → pair nil :: n__s:n__natsFrom:cons:nil u :: pair → a → n__s:n__natsFrom:cons:nil → b → pair activate :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil head :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil snd :: pair → n__s:n__natsFrom:cons:nil take :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil fst :: pair → n__s:n__natsFrom:cons:nil s :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil afterNth :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil tail :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil sel :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil const :: pair const1 :: a const2 :: b Rewrite Strategy: INNERMOST

(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(10) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: natsFrom(N) → cons(N, n__natsFrom(n__s(N))) [1] splitAt(0, XS) → pair(nil, XS) [1] u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS) [1] head(cons(N, XS)) → N [1] activate(X) → X [1] snd(pair(XS, YS)) → YS [1] take(0, XS) → fst(pair(nil, XS)) [2] activate(n__s(X)) → s(X) [2] activate(n__s(n__s(X'))) → s(s(activate(X'))) [2] activate(n__s(n__natsFrom(X''))) → s(natsFrom(activate(X''))) [2] afterNth(0, XS) → snd(pair(nil, XS)) [2] activate(n__natsFrom(X)) → natsFrom(X) [2] activate(n__natsFrom(n__s(X1))) → natsFrom(s(activate(X1))) [2] activate(n__natsFrom(n__natsFrom(X2))) → natsFrom(natsFrom(activate(X2))) [2] s(X) → n__s(X) [1] fst(pair(XS, YS)) → XS [1] tail(cons(N, XS)) → activate(XS) [1] natsFrom(X) → n__natsFrom(X) [1] sel(N, XS) → head(snd(splitAt(N, XS))) [2] snd(v0) → nil [0] The TRS has the following type information: natsFrom :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil cons :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil n__natsFrom :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil n__s :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil splitAt :: 0 → n__s:n__natsFrom:cons:nil → pair 0 :: 0 pair :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil → pair nil :: n__s:n__natsFrom:cons:nil u :: pair → a → n__s:n__natsFrom:cons:nil → b → pair activate :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil head :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil snd :: pair → n__s:n__natsFrom:cons:nil take :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil fst :: pair → n__s:n__natsFrom:cons:nil s :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil afterNth :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil tail :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil sel :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil const :: pair const1 :: a const2 :: b Rewrite Strategy: INNERMOST

(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
nil => 0
const => 0
const1 => 0
const2 => 0

(12) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ s(s(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ s(natsFrom(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ natsFrom(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(X1))) :|: X1 >= 0, z = 1 + (1 + X1)
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(X2))) :|: z = 1 + (1 + X2), X2 >= 0
afterNth(z, z') -{ 2 }→ snd(1 + 0 + XS) :|: z' = XS, z = 0, XS >= 0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
natsFrom(z) -{ 1 }→ 1 + N + (1 + (1 + N)) :|: z = N, N >= 0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sel(z, z') -{ 2 }→ head(snd(splitAt(N, XS))) :|: z' = XS, z = N, XS >= 0, N >= 0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
splitAt(z, z') -{ 1 }→ 1 + 0 + XS :|: z' = XS, z = 0, XS >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 2 }→ fst(1 + 0 + XS) :|: z' = XS, z = 0, XS >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(X) + YS) + ZS :|: z = 1 + YS + ZS, z'' = X, YS >= 0, X >= 0, z' = N, z1 = XS, ZS >= 0, XS >= 0, N >= 0

(13) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

natsFrom(z) -{ 1 }→ 1 + N + (1 + (1 + N)) :|: z = N, N >= 0
natsFrom(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
splitAt(z, z') -{ 1 }→ 1 + 0 + XS :|: z' = XS, z = 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0

(14) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ s(s(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ s(natsFrom(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(X1))) :|: X1 >= 0, z = 1 + (1 + X1)
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(X2))) :|: z = 1 + (1 + X2), X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z = 1 + X, X >= 0, X = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z' = XS, z = 0, XS >= 0, 1 + 0 + XS = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z' = XS, z = 0, XS >= 0, v0 >= 0, 1 + 0 + XS = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
natsFrom(z) -{ 1 }→ 1 + N + (1 + (1 + N)) :|: z = N, N >= 0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sel(z, z') -{ 4 }→ head(YS) :|: z' = XS, z = N, XS >= 0, N >= 0, XS = XS', N = 0, XS' >= 0, 1 + 0 + XS' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' = XS, z = N, XS >= 0, N >= 0, XS = XS', N = 0, XS' >= 0, v0 >= 0, 1 + 0 + XS' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
splitAt(z, z') -{ 1 }→ 1 + 0 + XS :|: z' = XS, z = 0, XS >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z' = XS, z = 0, XS >= 0, 1 + 0 + XS = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(X) + YS) + ZS :|: z = 1 + YS + ZS, z'' = X, YS >= 0, X >= 0, z' = N, z1 = XS, ZS >= 0, XS >= 0, N >= 0

(15) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(16) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

(17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ natsFrom } { snd } { take } { fst } { splitAt } { s } { afterNth } { head } { activate } { sel } { tail } { u }

(18) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {natsFrom}, {snd}, {take}, {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: natsFrom
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 3 + 2·z

(20) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {natsFrom}, {snd}, {take}, {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: ?, size: O(n1) [3 + 2·z]

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: natsFrom
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(22) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {snd}, {take}, {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z]

(23) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(24) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {snd}, {take}, {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z]

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: snd
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(26) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {snd}, {take}, {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: ?, size: O(n1) [z]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: snd
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(28) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {take}, {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z]

(29) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(30) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {take}, {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z]

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: take
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z'

(32) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {take}, {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: ?, size: O(n1) [z']

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: take
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 3

(34) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z']

(35) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(36) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z']

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: fst
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(38) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {fst}, {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: ?, size: O(n1) [z]

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: fst
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(40) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z]

(41) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(42) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z]

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: splitAt
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z'

(44) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {splitAt}, {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: ?, size: O(n1) [1 + z']

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: splitAt
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(46) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z']

(47) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(48) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z']

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: s
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(50) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {s}, {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: ?, size: O(n1) [1 + z]

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: s
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(52) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z]

(53) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(54) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z]

(55) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: afterNth
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z'

(56) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {afterNth}, {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: ?, size: O(n1) [z']

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: afterNth
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 5

(58) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z']

(59) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(60) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z']

(61) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: head
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(62) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {head}, {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: ?, size: O(n1) [z]

(63) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: head
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(64) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z]

(65) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(66) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z]

(67) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: EXP with polynomial bound: ?

(68) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {activate}, {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: ?, size: EXP

(69) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 7 + 4·z

(70) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP

(71) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(72) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP

(73) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: sel
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z'

(74) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {sel}, {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: ?, size: O(n1) [z']

(75) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: sel
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 9

(76) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z']

(77) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(78) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z']

(79) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: tail
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

(80) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {tail}, {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: ?, size: INF

(81) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: tail
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 4 + 4·z

(82) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: O(n1) [4 + 4·z], size: INF

(83) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(84) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: O(n1) [4 + 4·z], size: INF

(85) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: u
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

(86) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed: {u}
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: O(n1) [4 + 4·z], size: INF u: runtime: ?, size: INF

(87) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: u
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 8 + 4·z''

(88) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0

Function symbols to be analyzed:
Previous analysis results are:

natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: O(n1) [4 + 4·z], size: INF u: runtime: O(n1) [8 + 4·z''], size: INF

(89) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(90) BOUNDS(1, n^1)